i:Id, k:Knd. locknd(i;k)  LocKnd 

latex

Definitions	x:A. B(x), t  T, LocKnd, locknd(i;k), kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), if b then t else f fi , islocal(k), lnk(k), b, isl(x), t.1, outl(x), tt, ff, P  Q, Knd, b, x(s), x(s1,s2), P  Q, P & Q, P  Q, False, , rcv(l,tg), locl(a)
Lemmas	kindcase wf, Id wf, ldst wf, IdLnk wf, assert-hasloc, rcv wf, assert wf, isrcv wf, locl wf, hasloc wf, Knd wf